#pragma once
#include "PDTStatement.h"
#include "PDTExp.h"
#include "PDTBoolConst.h"

class PDTWhile  :  public PDTStatement, public TraverseIfc <PDTWhile , PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTWhile )
public:

  void
  setCondition(PDTExpBool & condition);

  void
  setLoopStatement(PDTStatement & loopStatement);

  PDTExpBool*
  getCondition() const;

  PDTStatement *
  getLoopStatement() const;

  PDTWhile(PDTCodeGraph & CG, PDTExpBool & condition,
      PDTStatement & loopStatement);

  NodeTypeEnum
  getType()
  {
    return PDTWhile_Em;
  }

  bool
  isWhile()
  {
    return true;
  }
  
  virtual bool eval(PDTCodeGraph &CG)
  {

	  getCondition()->eval(CG);
	  bool condition = (dynamic_cast<PDTBoolConst*>(getCondition()->nValue))->getValue();
	  while(condition)
	  {
		  if (!(getLoopStatement()->eval(CG)))
			  return false;
		  getCondition()->eval(CG);
		  condition = (dynamic_cast<PDTBoolConst*>(getCondition()->nValue))->getValue();
	  }
	  return true;
  }

	virtual PDTNode* clone(PDTCodeGraph& CG)
	{
		PDTNode* toReturn;
		PDTExpBool* conditionClone = (PDTExpBool*)(getCondition()->clone(CG));
		PDTStatement* loopStatementClone = (PDTStatement*)(children[1]->clone(CG));
		toReturn = new PDTWhile(CG, *conditionClone, *loopStatementClone);
		//incrementCloneID();
		//untouch();
		return toReturn;
	}

  virtual stringstream &
  toString(stringstream & ss) const
  {
    ss << "while (";
    getCondition()->toString(ss);
    ss << ") {" << endl;
    getLoopStatement()->toString(ss);
    ss << endl << "}";
    return ss;
  }

  virtual Z3_ast
  Z3NodeVisit (PDTZ3Visitor &ZV);
};
